Automating Refinement of Circus Programs
Identifieur interne : 000100 ( Main/Exploration ); précédent : 000099; suivant : 000101Automating Refinement of Circus Programs
Auteurs : Frank Zeyda [Royaume-Uni] ; Ana Cavalcanti [Royaume-Uni]Source :
- Lecture Notes in Computer Science [ 0302-9743 ] ; 2011.
English descriptors
- KwdEn :
Abstract
Abstract: In previous work, we have presented a mechanisation of Circus for the theorem prover ProofPowerZ . Circus is a refinement language for state-rich reactive systems that combines Z and CSP. In this paper, we present techniques to automate the discharge of proof obligations typically generated by the Circus refinement laws. They eliminate most of the proofs that are imposed by the fact that the encoding has to be precise about typing and well-definedness issues, and leave just those that are expected in a pen-and-paper refinement. This allows us to concentrate on the proof of properties that are significant for the problem at hand, while benefiting from the increased assurance and efficiency afforded by the use of a theorem prover as well as high-level tactic languages for refinement. Our case study is a refinement strategy for verification of control systems; we present the result of several experiments.
Url:
DOI: 10.1007/978-3-642-19829-8_18
Affiliations:
Links toward previous steps (curation, corpus...)
Le document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title xml:lang="en">Automating Refinement of Circus Programs</title><author><name sortKey="Zeyda, Frank" sort="Zeyda, Frank" uniqKey="Zeyda F" first="Frank" last="Zeyda">Frank Zeyda</name></author><author><name sortKey="Cavalcanti, Ana" sort="Cavalcanti, Ana" uniqKey="Cavalcanti A" first="Ana" last="Cavalcanti">Ana Cavalcanti</name></author></titleStmt><publicationStmt><idno type="wicri:source">ISTEX</idno><idno type="RBID">ISTEX:EE7612B8FA073B2BAFD7CBE5D1D00AF1DCFD4F77</idno><date when="2011" year="2011">2011</date><idno type="doi">10.1007/978-3-642-19829-8_18</idno><idno type="url">https://api.istex.fr/document/EE7612B8FA073B2BAFD7CBE5D1D00AF1DCFD4F77/fulltext/pdf</idno><idno type="wicri:Area/Main/Corpus">000A29</idno><idno type="wicri:explorRef" wicri:stream="Main" wicri:step="Corpus" wicri:corpus="ISTEX">000A29</idno><idno type="wicri:Area/Main/Curation">000A29</idno><idno type="wicri:Area/Main/Exploration">000100</idno><idno type="wicri:explorRef" wicri:stream="Main" wicri:step="Exploration">000100</idno></publicationStmt><sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">Automating Refinement of Circus Programs</title><author><name sortKey="Zeyda, Frank" sort="Zeyda, Frank" uniqKey="Zeyda F" first="Frank" last="Zeyda">Frank Zeyda</name><affiliation wicri:level="1"><country xml:lang="fr">Royaume-Uni</country><wicri:regionArea>University of York, Heslington, YO10 5DD, York</wicri:regionArea><wicri:noRegion>York</wicri:noRegion></affiliation><affiliation wicri:level="1"><country wicri:rule="url">Royaume-Uni</country></affiliation></author><author><name sortKey="Cavalcanti, Ana" sort="Cavalcanti, Ana" uniqKey="Cavalcanti A" first="Ana" last="Cavalcanti">Ana Cavalcanti</name><affiliation wicri:level="1"><country xml:lang="fr">Royaume-Uni</country><wicri:regionArea>University of York, Heslington, YO10 5DD, York</wicri:regionArea><wicri:noRegion>York</wicri:noRegion></affiliation><affiliation wicri:level="1"><country wicri:rule="url">Royaume-Uni</country></affiliation></author></analytic><monogr></monogr><series><title level="s">Lecture Notes in Computer Science</title><imprint><date>2011</date></imprint><idno type="ISSN">0302-9743</idno><idno type="eISSN">1611-3349</idno><idno type="ISSN">0302-9743</idno></series><idno type="istex">EE7612B8FA073B2BAFD7CBE5D1D00AF1DCFD4F77</idno><idno type="DOI">10.1007/978-3-642-19829-8_18</idno><idno type="ChapterID">Chap18</idno><idno type="ChapterID">18</idno></biblStruct></sourceDesc><seriesStmt><idno type="ISSN">0302-9743</idno></seriesStmt></fileDesc><profileDesc><textClass><keywords scheme="KwdEn" xml:lang="en"><term> ArcAngel C </term><term> ProofPower </term><term>tactics</term><term>theorem proving</term></keywords></textClass><langUsage><language ident="en">en</language></langUsage></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">Abstract: In previous work, we have presented a mechanisation of Circus for the theorem prover ProofPowerZ . Circus is a refinement language for state-rich reactive systems that combines Z and CSP. In this paper, we present techniques to automate the discharge of proof obligations typically generated by the Circus refinement laws. They eliminate most of the proofs that are imposed by the fact that the encoding has to be precise about typing and well-definedness issues, and leave just those that are expected in a pen-and-paper refinement. This allows us to concentrate on the proof of properties that are significant for the problem at hand, while benefiting from the increased assurance and efficiency afforded by the use of a theorem prover as well as high-level tactic languages for refinement. Our case study is a refinement strategy for verification of control systems; we present the result of several experiments.</div></front></TEI><affiliations><list><country><li>Royaume-Uni</li></country></list><tree><country name="Royaume-Uni"><noRegion><name sortKey="Zeyda, Frank" sort="Zeyda, Frank" uniqKey="Zeyda F" first="Frank" last="Zeyda">Frank Zeyda</name></noRegion><name sortKey="Cavalcanti, Ana" sort="Cavalcanti, Ana" uniqKey="Cavalcanti A" first="Ana" last="Cavalcanti">Ana Cavalcanti</name><name sortKey="Cavalcanti, Ana" sort="Cavalcanti, Ana" uniqKey="Cavalcanti A" first="Ana" last="Cavalcanti">Ana Cavalcanti</name><name sortKey="Zeyda, Frank" sort="Zeyda, Frank" uniqKey="Zeyda F" first="Frank" last="Zeyda">Frank Zeyda</name></country></tree></affiliations></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Wicri/explor/CircusV2/Data/Main/Exploration
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 000100 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Exploration/biblio.hfd -nk 000100 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Wicri
|area= CircusV2
|flux= Main
|étape= Exploration
|type= RBID
|clé= ISTEX:EE7612B8FA073B2BAFD7CBE5D1D00AF1DCFD4F77
|texte= Automating Refinement of Circus Programs
}}
| This area was generated with Dilib version V0.6.31. |  |